Skip to content

perf(Tactic/FastInstance): use whnf on data fields#37924

Open
JovanGerb wants to merge 3 commits intoleanprover-community:masterfrom
JovanGerb:Jovan-fast_instance-whnf
Open

perf(Tactic/FastInstance): use whnf on data fields#37924
JovanGerb wants to merge 3 commits intoleanprover-community:masterfrom
JovanGerb:Jovan-fast_instance-whnf

Conversation

@JovanGerb
Copy link
Copy Markdown
Contributor

@JovanGerb JovanGerb commented Apr 11, 2026 •
edited
Loading

This PR lets fast_instance% make even faster instances by using whnf on data fields.

This PR also changes withReducible to the more appropriate withReducibleAndInstances in the implementation.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 11, 2026 •
edited
Loading

PR summary b1b1f5f52d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions Bot added the t-meta Tactics, attributes or user commands label Apr 11, 2026
@JovanGerb JovanGerb added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 11, 2026
@JovanGerb
Copy link
Copy Markdown
Contributor Author

JovanGerb commented Apr 11, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 11, 2026 •
edited
Loading

Benchmark results for e283a60 against b1b1f5f are in. Significant changes detected! @JovanGerb

  • ✅ build//instructions: -154.8G (-0.09%)

Large changes (1✅)

  • ✅ build/module/Mathlib.Algebra.Order.Ring.StandardPart//instructions: -57.2G (-34.55%)

Medium changes (7✅, 4🟥)

  • 🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic//instructions: +1.9G (+7.65%)
  • 🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula//instructions: +3.2G (+5.63%)
  • 🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point//instructions: +8.2G (+7.06%)
  • 🟥 build/module/Mathlib.Analysis.CStarAlgebra.lpSpace//instructions: +1.7G (+7.79%)
  • ✅ build/module/Mathlib.FieldTheory.Galois.Profinite//instructions: -2.5G (-3.60%)
  • ✅ build/module/Mathlib.FieldTheory.IntermediateField.Algebraic//instructions: -3.8G (-8.37%)
  • ✅ build/module/Mathlib.FieldTheory.RatFunc.IntermediateField//instructions: -2.9G (-5.42%)
  • ✅ build/module/Mathlib.FieldTheory.Relrank//instructions: -5.4G (-5.32%)
  • ✅ build/module/Mathlib.FieldTheory.SeparableClosure//instructions: -8.4G (-7.05%)
  • ✅ build/module/Mathlib.NumberTheory.NumberField.CMField//instructions: -7.4G (-7.42%)
  • ✅ build/module/Mathlib.NumberTheory.NumberField.Completion.InfinitePlace//instructions: -3.5G (-7.42%)

Small changes (25✅, 6🟥)

Too many entries to display here. View the full report on radar instead.

@github-actions github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 11, 2026
@JovanGerb
Copy link
Copy Markdown
Contributor Author

JovanGerb commented Apr 11, 2026

That's a nice speedup, but it's worrying that there's also a slowdown.

joneugster
joneugster reviewed Apr 24, 2026
View reviewed changes
Comment thread Mathlib/Tactic/FastInstance.lean
-- This is an invalid term.
throwError "Incorrect number of arguments for constructor application `{f}`: {args}"
-- Unify the parameters
unless ← isDefEq expectedType cls do
Copy link
Copy Markdown
Contributor

@joneugster joneugster Apr 24, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

could it be that the slowdown in certain files could be explained by the changed transparency which affects a few places, like this line here?

@joneugster joneugster assigned joneugster and unassigned dwrensha Apr 24, 2026
@joneugster joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 24, 2026
@JovanGerb JovanGerb added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 28, 2026
@JovanGerb
Copy link
Copy Markdown
Contributor Author

JovanGerb commented Apr 28, 2026

Good idea, let's see what difference it makes:

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 28, 2026 •
edited
Loading

Benchmark results for b6ad48a against b1b1f5f are in. There are significant results. @JovanGerb

  • ✅ build//instructions: -186.9G (-0.11%)

Large changes (1✅)

  • ✅ build/module/Mathlib.Algebra.Order.Ring.StandardPart//instructions: -56.9G (-34.36%)

Medium changes (7✅, 4🟥)

  • 🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic//instructions: +1.9G (+7.69%)
  • 🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula//instructions: +3.2G (+5.69%)
  • 🟥 build/module/Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point//instructions: +8.0G (+6.94%)
  • 🟥 build/module/Mathlib.Analysis.CStarAlgebra.lpSpace//instructions: +1.7G (+7.74%)
  • ✅ build/module/Mathlib.FieldTheory.Galois.Profinite//instructions: -2.5G (-3.61%)
  • ✅ build/module/Mathlib.FieldTheory.IntermediateField.Algebraic//instructions: -3.8G (-8.34%)
  • ✅ build/module/Mathlib.FieldTheory.RatFunc.IntermediateField//instructions: -2.8G (-5.29%)
  • ✅ build/module/Mathlib.FieldTheory.Relrank//instructions: -5.3G (-5.22%)
  • ✅ build/module/Mathlib.FieldTheory.SeparableClosure//instructions: -8.4G (-7.04%)
  • ✅ build/module/Mathlib.NumberTheory.NumberField.CMField//instructions: -7.5G (-7.46%)
  • ✅ build/module/Mathlib.NumberTheory.NumberField.Completion.InfinitePlace//instructions: -3.5G (-7.50%)

Small changes (27✅, 10🟥)

Too many entries to display here. View the full report on radar instead.

@github-actions github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 28, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@joneugster joneugster joneugster left review comments

Assignees

@joneugster joneugster

Labels

awaiting-author A reviewer has asked the author a question or requested changes. t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@JovanGerb @leanprover-radar @joneugster @dwrensha